theory k_mem_pool
imports Main
begin
  
datatype thread_state_type = READY | RUNNING | BLOCKED
datatype block_state_type = FREE | ALLOC | DIV
datatype timeout_state_type = WAIT | NO_WAIT | FOREVER
datatype 'a tree = Leaf 'a | Node 'a (LL:"'a tree") (LR:"'a tree") (RL:"'a tree") (RR:"'a tree")
typedecl ID
typedecl Thread
datatype poolname = "string"
  
type_synonym Block = "(nat \<times> block_state_type \<times> ID) tree"
type_synonym Level_Freelist = "(ID list) list"
  
record Pool = zerolevelblocklist :: "Block list"
              freelist :: "Level_Freelist"
              n_levels :: "nat"
              nmax :: "nat"
              name :: "poolname"
  
definition getnewid :: "ID set \<Rightarrow> (ID \<times> ID \<times> ID \<times> ID \<times> ID set)"
  where "getnewid ids \<equiv> let nid1 = SOME p1. p1 \<notin> ids;
                            ids1 = ids \<union> {nid1};
                            nid2 = SOME p2. p2 \<notin> ids1;
                            ids2 = ids1 \<union> {nid2};
                            nid3 = SOME p3. p3 \<notin> ids2;
                            ids3 = ids2 \<union> {nid3};
                            nid4 = SOME P4. P4 \<notin> ids3;
                            ids4 = ids3 \<union> {nid4} in
                        (nid1, nid2, nid3, nid4, ids4)"
    
definition getnewid2 :: "ID set \<Rightarrow> (ID \<times> ID set)"
  where "getnewid2 ids \<equiv> let nid = SOME p. p \<notin> ids;
                             nids = ids \<union> {nid} in
                             (nid, nids)"

definition divide :: "Block \<Rightarrow> Level_Freelist \<Rightarrow> ID set \<Rightarrow> (Block \<times> Level_Freelist \<times> ID set)"
  where "divide b li ids \<equiv> case b of (Leaf (level, FREE, x))
                         \<Rightarrow> let l_freelist = tl (li ! level);
                                (x1,x2,x3,x4,newids) = getnewid ids;
                                nextl_freelist = append (li ! (Suc level)) [x1, x2, x3, x4] in
                           (Node (level, DIV, x) (Leaf (Suc level, FREE, x1)) (Leaf (Suc level, FREE, x2)) (Leaf (Suc level, FREE, x3)) (Leaf (Suc level, FREE, x4)),
                           (li[level:=l_freelist])[(Suc level):= nextl_freelist],
                           newids)"
  
definition combine :: "Block \<Rightarrow> Level_Freelist \<Rightarrow> ID set \<Rightarrow> (Block \<times> Level_Freelist \<times> ID set)"
  where "combine b li ids \<equiv> case b of Node (level, DIV, x) (Leaf (_, FREE, x1)) (Leaf (_, FREE, x2)) (Leaf (_, FREE, x3)) (Leaf (_, FREE, x4))
                            \<Rightarrow> let l_freelist = append (li ! level) [x];
                                   nextl_freelist = remove1 x4 (remove1 x3 (remove1 x2 (remove1 x1 (li ! Suc level))));
                                   nids = (((ids - {x1}) - {x2}) - {x3}) - {x4} in
                               (Leaf (level, FREE, x), (li[level:=l_freelist])[(Suc level):= nextl_freelist], nids)"
    
primrec get_level :: "Block \<Rightarrow> nat"
    where "get_level (Leaf a) = fst a" |
          "get_level (Node a ll lr rl rr) = fst a"
          
primrec get_blocktype :: "Block \<Rightarrow> block_state_type"
  where "get_blocktype (Leaf a) = fst (snd a)" |
        "get_blocktype (Node a ll lr rl rr) = fst (snd a)"

definition get_first_freeblock :: "Level_Freelist \<Rightarrow> nat \<Rightarrow> ID"
  where "get_first_freeblock li lv \<equiv> let l_freelist = (li ! lv) in
                                     case l_freelist of [x,_] \<Rightarrow> x"
    
definition delete_first_freeblock :: "Level_Freelist \<Rightarrow> nat \<Rightarrow> Level_Freelist"
  where "delete_first_freeblock li lv \<equiv> let l_freelist = (li ! lv) in
                                        case l_freelist of [] \<Rightarrow> li
                                                        | _ \<Rightarrow> li[lv:=(tl l_freelist)]"
        
function alloc :: "Block \<Rightarrow> Level_Freelist \<Rightarrow> nat \<Rightarrow> ID set \<Rightarrow> (Block \<times> Level_Freelist \<times> ID set \<times> bool)"
  where "alloc (Leaf v) li lv ids = (if lv < get_level (Leaf v) then (Leaf v, li, ids, False)
                                    else if lv = get_level (Leaf v) then
                                      if fst (snd v) = FREE  \<and> snd (snd v) = get_first_freeblock li lv 
                                        then (Leaf (fst v, ALLOC, snd (snd v)), delete_first_freeblock li lv, ids, True) 
                                      else (Leaf v, li, ids, False)
                                    else 
                                      if fst (snd v) = ALLOC then (Leaf v, li, ids, False)
                                      else
                                        let (node,freelist,newids) = divide (Leaf v) li ids in
                                        case node of (Node a ll lr rl rr) \<Rightarrow>
                                          let c1 = alloc ll freelist lv newids in
                                          if snd (snd (snd c1)) then (Node a (fst c1) lr rl rr, fst (snd c1), fst (snd (snd c1)), True)
                                          else
                                            let c2 = alloc lr freelist lv newids in
                                            if snd (snd (snd c2)) then (Node a ll (fst c2) rl rr, fst (snd c2), fst (snd (snd c2)), True)
                                            else
                                              let c3 = alloc rl freelist lv newids in
                                              if snd (snd (snd c3)) then (Node a ll lr (fst c3) rr, fst (snd c3), fst (snd (snd c3)), True)
                                              else
                                                let c4 = alloc rr freelist lv newids in
                                                if snd (snd (snd c4)) then (Node a ll lr rl (fst c4), fst (snd c4), fst (snd (snd c4)), True)
                                                else (Node a ll lr rl rr, freelist, newids, False))" |
        "alloc (Node a ll lr rl rr) li lv ids = (let c1 = alloc ll li lv ids in
                                                if snd (snd (snd c1)) then (Node a (fst c1) lr rl rr, fst (snd c1), fst (snd (snd c1)), True)
                                                else
                                                  let c2 = alloc lr li lv ids in
                                                  if snd (snd (snd c2)) then (Node a ll (fst c2) rl rr, fst (snd c2), fst (snd (snd c2)), True)
                                                  else
                                                    let c3 = alloc rl li lv ids in
                                                    if snd (snd (snd c3)) then (Node a ll lr (fst c3) rr, fst (snd c3), fst (snd (snd c3)), True)
                                                    else
                                                      let c4 = alloc rr li lv ids in
                                                      if snd (snd (snd c4)) then (Node a ll lr rl (fst c4), fst (snd c4), fst (snd (snd c4)), True)
                                                      else (Node a ll lr rl rr, li, ids, False))"
  sorry
termination sorry

function pool_alloc :: "Pool \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ID set \<Rightarrow> (Pool \<times> ID set \<times> bool)"
  where "pool_alloc po lv n ids = (if lv < 0 then (po, ids, False)
                                  else
                                    let zeroli = zerolevelblocklist po;
                                        freeli = freelist po;
                                        len = nmax po;
                                        (bl,fl,newids,re) = alloc (zeroli ! n) freeli lv ids in
                                        if re = True \<and> n < len then
                                          (po\<lparr>zerolevelblocklist := zeroli[n:=bl], freelist := fl\<rparr>, newids, True)
                                        else if re = False \<and> n < (len-1) then
                                          let newn = Suc n in
                                          pool_alloc po lv newn ids
                                        else
                                          (po, ids, False))"
  sorry
termination sorry
  
function free :: "Block \<Rightarrow> Level_Freelist \<Rightarrow> ID \<Rightarrow> ID set \<Rightarrow> (Block \<times> Level_Freelist \<times> ID set \<times> bool)"
  where "free (Leaf v) li num ids = (if fst (snd v) = ALLOC \<and> snd (snd v) = num
                                    then 
                                      let l_freelist = append (li ! (fst v)) [snd (snd v)] in
                                      (Leaf (fst v, FREE, snd (snd v)), li[(fst v):=l_freelist], ids, True)
                                    else
                                      (Leaf v, li, ids, False))" |
        "free (Node a ll lr rl rr) li num ids = (let c1 = free ll li num ids in
                                                if snd (snd (snd c1)) then
                                                  case (Node a (fst c1) lr rl rr) of Node (_, DIV, _) (Leaf (_, FREE, _)) (Leaf (_, FREE, _)) (Leaf (_, FREE, _)) (Leaf (_, FREE, _))
                                                             \<Rightarrow> let (node,freelist,nids) = combine (Node a (fst c1) lr rl rr) (fst (snd c1)) (fst (snd (snd c1))) in
                                                                (node, freelist, nids, True)
                                                         | _ \<Rightarrow> (Node a (fst c1) lr rl rr, fst (snd c1), (fst (snd (snd c1))), True)
                                                else
                                                  let c2 = free lr li num ids in
                                                    if snd (snd (snd c2)) then
                                                      case (Node a ll (fst c2) rl rr) of Node (_, DIV, _) (Leaf (_, FREE, _)) (Leaf (_, FREE, _)) (Leaf (_, FREE, _)) (Leaf (_, FREE, _))
                                                                \<Rightarrow> let (node,freelist,nids) = combine (Node a ll (fst c2) rl rr) (fst (snd c2)) (fst (snd (snd c2))) in
                                                                       (node, freelist, nids, True)
                                                            | _ \<Rightarrow> (Node a ll (fst c2) rl rr, fst (snd c2), (fst (snd (snd c2))), True)
                                                    else
                                                      let c3 = free rl li num ids in
                                                        if snd (snd (snd c3)) then
                                                          case (Node a ll lr (fst c3) rr) of Node (_, DIV, _) (Leaf (_, FREE, _)) (Leaf (_, FREE, _)) (Leaf (_, FREE, _)) (Leaf (_, FREE, _))
                                                                    \<Rightarrow> let (node,freelist,nids) = combine (Node a ll lr (fst c3) rr) (fst (snd c3)) (fst (snd (snd c3))) in
                                                                           (node, freelist, nids, True)
                                                                | _ \<Rightarrow> (Node a ll lr (fst c3) rr, fst (snd c3), (fst (snd (snd c3))), True)
                                                        else
                                                          let c4 = free rr li num ids in
                                                            if snd (snd (snd c4)) then
                                                              case (Node a ll lr rl (fst c4)) of Node (_, DIV, _) (Leaf (_, FREE, _)) (Leaf (_, FREE, _)) (Leaf (_, FREE, _)) (Leaf (_, FREE, _))
                                                                        \<Rightarrow> let (node,freelist,nids) = combine (Node a ll lr rl (fst c4)) (fst (snd c4)) (fst (snd (snd c4))) in
                                                                               (node, freelist, nids, True)
                                                                    | _ \<Rightarrow> (Node a ll lr rl (fst c4), fst (snd c4), (fst (snd (snd c4))), True)
                                                            else (Node a ll lr rl rr, li, ids, False))"
  sorry
termination sorry
    
function pool_free :: "Pool \<Rightarrow> ID \<Rightarrow> nat \<Rightarrow> ID set \<Rightarrow> (Pool \<times> ID set \<times> bool)"
  where "pool_free po num n ids = (let zeroli = zerolevelblocklist po;
                                       freeli = freelist po;
                                       len = nmax po;
                                       (bl,fl,nids,re) = free (zeroli ! n) freeli num ids in
                                       if re = True \<and> n < len then
                                         (po\<lparr>zerolevelblocklist := zeroli[n:= bl], freelist := fl\<rparr>, nids, True)
                                       else if re = False \<and> n < (len-1) then
                                         let newn = Suc n in
                                         pool_free po num newn ids
                                       else
                                         (po, ids, False))"
  sorry
termination sorry

record State = t_state :: "Thread \<Rightarrow> thread_state_type"
               pools :: "Pool list"
               waitq :: "Thread \<rightharpoonup> poolname"
               cur :: Thread
               tick :: nat
               idset :: "ID set"

consts s0 :: "State"
specification(s0)
    threadstate: "\<forall>th. (th \<noteq> (cur s0) \<longrightarrow> (t_state s0) th = READY) \<and> (th = (cur s0) \<longrightarrow> (t_state s0) th = RUNNING)"
    poolsinit: "pools s0 = []"
    waitqinit: "dom (waitq s0) = {}"
    tickinit: "tick s0 = 0"
    idsetinit: "idset s0 = {}"
sorry

definition time_tick :: "State \<Rightarrow> State"
  where "time_tick s \<equiv> let ti = Suc (tick s) in
                         s\<lparr>tick := ti\<rparr>"
    
definition schedule :: "State \<Rightarrow> State"
  where "schedule s \<equiv> let t = cur s;
                          news = s\<lparr>t_state := (t_state s)(t := READY)\<rparr>;
                          newcur = SOME p. p \<in> {t. (t_state news t) = READY} in
                       news\<lparr>t_state := (t_state news)(newcur := RUNNING),
                            cur := newcur\<rparr>"
                  
definition k_mem_pool_alloc :: "State \<Rightarrow> Pool \<Rightarrow> nat \<Rightarrow> timeout_state_type \<Rightarrow> (State \<times> bool)"
  where "k_mem_pool_alloc s po lv ti \<equiv> if lv < 0 then (s,False)
                                       else
                                         let ts = t_state s;
                                             ps = pools s;
                                             wq = waitq s;
                                             cu = cur s;
                                             ids = idset s;
                                             rpi = pool_alloc po lv 0 ids in
                                         if snd (snd rpi) = True then
                                           (s\<lparr>pools := append (remove1 po ps) [fst rpi],
                                              idset := fst (snd rpi)\<rparr>, True)
                                         else if snd (snd rpi) = False \<and> (ti = WAIT \<or> ti = FOREVER) then
                                            let t = s\<lparr>t_state := ts(cu := BLOCKED),
                                              waitq := wq(cu := Some (name po))\<rparr> in
                                            (schedule t, False)
                                         else
                                           (s, False)"
    
definition k_mem_pool_free :: "State \<Rightarrow> Pool \<Rightarrow> ID \<Rightarrow> (State \<times> bool)"
  where "k_mem_pool_free s po num \<equiv> let ts = t_state s;
                                         ps = pools s;
                                         wq = waitq s;
                                         ids = idset s;
                                         npi = pool_free po num 0 ids in
                                         if snd (snd npi) = True then
                                           let wqth = {t. wq t = Some (name po)} in
                                           if wqth \<noteq> {} then
                                             (s\<lparr>t_state := (\<lambda>t. (if (t \<in> wqth) then READY else (ts t))),
                                                pools := append (remove1 po ps) [fst npi],
                                                waitq := (\<lambda>t. (if (t \<in> wqth) then None else (wq t))),
                                                idset := fst (snd npi)\<rparr>,True)
                                           else
                                             (s\<lparr>pools := append (remove1 po ps) [fst npi],
                                                idset := fst (snd npi)\<rparr>, True)
                                         else
                                           (s, False)"

function pool_init :: "Block list \<Rightarrow> ID list \<Rightarrow> nat \<Rightarrow> ID set \<Rightarrow> nat \<Rightarrow> (Block list \<times> ID list \<times> ID set)"
  where "pool_init bli idl nm ids num = (if nm = 0 then (bli,idl,ids)
                                         else
                                           let (nid,nids) = getnewid2 ids;
                                               b = Leaf(0, FREE, nid);
                                               newbli = append bli [b];
                                               newidl = append idl [nid] in
                                               if num < (nm-1) then
                                                 let newnum = Suc num in
                                                 (pool_init newbli newidl nm nids newnum)
                                               else (newbli,newidl,nids))"
  sorry
termination sorry

definition K_MEM_POOL_DEFINE :: "State \<Rightarrow> poolname \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (State \<times> bool)"
  where "K_MEM_POOL_DEFINE s nam nlv num \<equiv> let ids = idset s;
                                               rnids = getnewid2 ids;
                                               bli = [Leaf(0,FREE,fst rnids)];
                                               idl = [fst rnids];
                                               rpi = pool_init bli idl (num-1) (snd rnids) 0;
                                               po = \<lparr>zerolevelblocklist = fst rpi,
                                                     freelist = SOME fli::Level_Freelist. (length fli = nlv) \<and> (fli ! 0 = fst (snd rpi)),
                                                     n_levels = nlv,
                                                     nmax = num,
                                                     name = nam\<rparr>;
                                               ps = pools s in
                                            (s\<lparr>pools := append ps [po],
                                               idset := snd (snd rpi)\<rparr>, True)"

type_synonym Trace = "State list"
inductive_set execution :: "Trace set" where
  zero: "[s] \<in> execution" |
  
  init: "\<lbrakk>es \<in> execution; fst (K_MEM_POOL_DEFINE s nam nlv num) = t; t = es ! 0\<rbrakk> \<Longrightarrow>
         s # es \<in> execution" |
  
  alloc1: "\<lbrakk>es \<in> execution; fst (k_mem_pool_alloc s po lv ti) = t; t = es ! 0\<rbrakk> \<Longrightarrow>
           s # es \<in> execution" |
  
  free1: "\<lbrakk>es \<in> execution; fst (k_mem_pool_free s po num) = t; t = es ! 0\<rbrakk> \<Longrightarrow>
          s # es \<in> execution" |
  
  titi: "\<lbrakk>es \<in> execution; time_tick s = t; t = es ! 0\<rbrakk> \<Longrightarrow>
         s # es \<in> execution" |
  
  sche: "\<lbrakk>es \<in> execution; schedule s = t; t = es ! 0\<rbrakk> \<Longrightarrow>
         s # es \<in> execution"


lemma exec_not_empty: "ts\<in>execution \<Longrightarrow> ts \<noteq> []"
  apply(rule execution.cases)
    apply simp +
  done

definition "reachable s t \<equiv> (\<exists>ts \<in> execution. ts ! 0 = s \<and> last ts = t)"

definition "reachable0 s \<equiv> reachable s0 s"
 
lemma "reachable0 s0"
  unfolding reachable0_def reachable_def using zero by force

definition "ReachStates \<equiv> {s. reachable0 s}"
  
(*
subsection \<open>correctness of k_mem_pool_define\<close>

definition "Precond_MemPoolInit \<equiv> {s. True}"
definition "Postcond_MemPoolInit \<equiv> {s. True}"

lemma "s\<in>Precond_MemPoolInit \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nlv num) \<in> Postcond_MemPoolInit"
  sorry
*)

subsection \<open>def and proof of inv_cur_state\<close>

definition "inv_cur_state \<equiv> {s::State. t_state s (cur s) = RUNNING}"

lemma inv_cur_s0: "s0 \<in> inv_cur_state"
  unfolding s0_def inv_cur_state_def using s0_def threadstate by auto

lemma inv_cur_k_mem_pool_define: "s \<in> inv_cur_state \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv_cur_state"
  unfolding K_MEM_POOL_DEFINE_def Let_def inv_cur_state_def by auto

lemma inv_cur_time_tick: "s \<in> inv_cur_state \<Longrightarrow> time_tick s \<in> inv_cur_state"
  unfolding time_tick_def Let_def inv_cur_state_def by auto
    
lemma inv_cur_schedule: "s \<in> inv_cur_state \<Longrightarrow> schedule s \<in> inv_cur_state"
  unfolding schedule_def Let_def inv_cur_state_def by auto
    
lemma inv_cur_k_mem_pool_alloc: "s \<in> inv_cur_state \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv_cur_state" 
proof (induct ti)
  case  WAIT
    then show ?case unfolding k_mem_pool_alloc_def Let_def
      by (smt State.select_convs(1) State.select_convs(4) State.surjective State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(6) fst_conv fun_upd_same inv_cur_state_def mem_Collect_eq schedule_def)
  case FOREVER
    then show ?case unfolding k_mem_pool_alloc_def Let_def
      by (smt State.surjective State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(6) \<open>fst (k_mem_pool_alloc s po lv WAIT) \<in> inv_cur_state\<close> k_mem_pool_alloc_def) 
  case NO_WAIT
    then show ?case unfolding k_mem_pool_alloc_def Let_def
      by (simp add: inv_cur_state_def)
qed
    
lemma inv_cur_k_mem_pool_free: "s \<in> inv_cur_state \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv_cur_state"
proof (cases "waitq s x = Some (name po)")
  case True
  then show ?thesis unfolding k_mem_pool_free_def Let_def 
next
  case False
  then show ?thesis sorry
qed
    
lemma inv_cur_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv_cur_state \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv_cur_state))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv_cur_state"
    then have "\<forall>i<length ts. ts ! i \<in> inv_cur_state"
      apply(induct ts)
       apply simp
      using inv_cur_k_mem_pool_define inv_cur_k_mem_pool_alloc inv_cur_k_mem_pool_free inv_cur_time_tick inv_cur_schedule
      apply (metis One_nat_def Suc_less_eq Suc_pred length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_cur_k_mem_pool_alloc length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_cur_k_mem_pool_free length_Cons neq0_conv nth_Cons')
      apply (metis (no_types, lifting) One_nat_def diff_less inv_cur_time_tick length_Cons less_Suc_eq less_le_trans nat_less_le neq0_conv nth.simps nth_Cons' nth_Cons_0)
      by (metis One_nat_def diff_less inv_cur_schedule length_Cons less_Suc_eq less_le_trans nat_less_le neq0_conv nth_Cons')
  }
  then show ?thesis by auto
qed

lemma inv_cur_lm: "ReachStates \<subseteq> inv_cur_state"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv_cur_state" using inv_cur_lm_helper inv_cur_s0
      by (metis append_butlast_last_id exec_not_empty length_append_singleton lessI nth_append_length)
  }
  then show ?thesis by auto
qed
     
subsection \<open>def and proof of inv_waitq_state\<close>

definition "inv_waitq_state \<equiv> {s::State. (\<forall>th. th \<in> dom(waitq s) \<longrightarrow> t_state s th = BLOCKED)}"

lemma inv_waitq_s0: "s0 \<in> inv_waitq_state"
  unfolding s0_def inv_waitq_state_def using s0_def waitqinit by auto
  
lemma inv_waitq_k_mem_pool_define: "s \<in> inv_waitq_state \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv_waitq_state"
proof -
  assume "s \<in> inv_waitq_state"
  hence p0: "\<forall>th. th \<in> dom(waitq s) \<longrightarrow> t_state s th = BLOCKED" 
    unfolding inv_waitq_state_def by simp
  let ?t = "fst (K_MEM_POOL_DEFINE s nam nlv num)"
  {
    fix th
    assume a0: "th \<in> dom (waitq ?t)"
    have "waitq s = waitq ?t" unfolding K_MEM_POOL_DEFINE_def
      by (simp add:Let_def) 
    moreover
    have "t_state s = t_state ?t" unfolding K_MEM_POOL_DEFINE_def 
      by (simp add:Let_def) 
    ultimately have "t_state ?t th = BLOCKED" using p0 a0 by force
  }
  then show ?thesis unfolding inv_waitq_state_def by auto
qed

lemma inv_waitq_time_tick: "s \<in> inv_waitq_state \<Longrightarrow> time_tick s \<in> inv_waitq_state"
  unfolding time_tick_def Let_def inv_waitq_state_def by auto
    
lemma inv_waitq_schedule: "s \<in> ReachStates \<and> s \<in> inv_waitq_state \<Longrightarrow> schedule s \<in> inv_waitq_state"
proof -
  assume "s \<in> ReachStates \<and> s \<in> inv_waitq_state"
  hence p0: "s \<in> inv_cur_state"
    and p1: "\<forall>th. th \<in> dom (waitq s) \<longrightarrow> t_state s th = BLOCKED"
    unfolding inv_waitq_state_def using inv_cur_lm by auto
  let ?t = "schedule s"
  {
    fix th
    assume a0: "th \<in> dom (waitq ?t)"
    have p2: "waitq s = waitq ?t" unfolding schedule_def Let_def by simp
    moreover
    have p3: "t_state s (cur s) = RUNNING" using inv_cur_state_def p0 by auto 
    have p4: "cur s \<notin> dom (waitq s)" using p1 p3 by auto  
    have p5: "\<forall>t. t_state s t = READY \<longrightarrow> t \<notin> dom (waitq s)" using p1 by auto 
    moreover
    have "cur s \<notin> dom (waitq ?t)" using p2 p4 by auto
    have "\<forall>t. t_state s t = READY \<longrightarrow> t \<notin> dom (waitq ?t)" using p2 p5 by auto 
    moreover
    have p7: "t_state s th \<noteq> READY" using a0 calculation(3) by auto 
    have p8: "cur s \<noteq> th" using a0 p2 p4 by auto 
    have p9: "t_state s th = BLOCKED" by (simp add: a0 p1 p2) 
    moreover  
    from p7 p8 p9 have "t_state ?t th = BLOCKED"
    proof -
      have f1: "\<forall>t ta f. (f(t::Thread := ta::thread_state_type)) (SOME tb. (f(t := ta)) tb = ta) = ta"
        by (meson fun_upd_apply tfl_some)
      have "((t_state s)(cur s := READY)) th \<noteq> READY \<and> ((t_state s)(cur s := READY)) th = BLOCKED"
        using p8 p9 by auto
      then have "(SOME t. t \<in> {t. ((t_state s)(cur s := READY)) t = READY}) \<noteq> th \<and> ((t_state s)(cur s := READY)) th = BLOCKED"
        using f1 by fastforce
      then show ?thesis unfolding schedule_def Let_def
        by fastforce
    qed      
  }
  then show ?thesis unfolding inv_waitq_state_def by auto
qed
  
lemma inv_waitq_k_mem_pool_alloc: "s \<in> inv_waitq_state \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv_waitq_state" 
proof (induct ti)
  case WAIT
  then show ?case unfolding k_mem_pool_alloc_def Let_def
    sorry
  case NO_WAIT
  then show ?case unfolding k_mem_pool_alloc_def Let_def
    by (smt State.surjective State.update_convs(2) State.update_convs(6) \<open>fst (k_mem_pool_alloc s po lv WAIT) \<in> inv_waitq_state\<close> fstI k_mem_pool_alloc_def timeout_state_type.distinct(1) timeout_state_type.distinct(5))
  case FOREVER
  then show ?case unfolding k_mem_pool_alloc_def Let_def
    by (smt State.surjective State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(6) \<open>fst (k_mem_pool_alloc s po lv WAIT) \<in> inv_waitq_state\<close> k_mem_pool_alloc_def)
qed
          
lemma inv_waitq_k_mem_pool_free: "s \<in> inv_waitq_state \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv_waitq_state" sorry
  
lemma inv_waitq_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv_waitq_state \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv_waitq_state))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv_waitq_state"
    then have "\<forall>i<length ts. ts ! i \<in> inv_waitq_state"
      apply(induct ts)
       apply simp
      using inv_waitq_k_mem_pool_define inv_waitq_k_mem_pool_alloc inv_waitq_k_mem_pool_free inv_waitq_time_tick inv_waitq_schedule
      apply (metis One_nat_def Suc_less_eq Suc_pred length_Cons neq0_conv nth_Cons' nth_Cons_0)
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_waitq_k_mem_pool_alloc length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_waitq_k_mem_pool_free length_Cons neq0_conv nth_Cons')
      apply (metis (no_types, lifting) One_nat_def diff_less inv_waitq_time_tick length_Cons less_Suc_eq less_le_trans nat_less_le neq0_conv nth.simps nth_Cons' nth_Cons_0)
      sorry
  }
  then show ?thesis by auto
qed

lemma inv_waitq_lm: "ReachStates \<subseteq> inv_waitq_state"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv_waitq_state" using inv_waitq_lm_helper inv_waitq_s0
    sorry
  }
  then show ?thesis by auto
qed

subsection \<open>def and proof of inv_block_state\<close>
  
primrec block_state :: "Block \<Rightarrow> bool"
  where "block_state (Leaf a) = (fst (snd a) = FREE \<or> fst (snd a) = ALLOC)" |
        "block_state (Node a ll lr rl rr) = (fst (snd a) = DIV \<and> block_state ll \<and> block_state lr \<and> block_state rl \<and> block_state rr)"
    
definition "inv_block_state \<equiv> {s::State. (\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). block_state b))}"

lemma inv_block_s0: "s0 \<in> inv_block_state"
  unfolding s0_def inv_block_state_def block_state_def using s0_def poolsinit by auto
    
lemma inv_block_k_mem_pool_define: "s \<in> inv_block_state \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv_block_state"
proof -
  assume "s \<in> inv_block_state"
  hence p0: "\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). block_state b)" 
    unfolding inv_block_state_def by auto
  let ?t = "fst (K_MEM_POOL_DEFINE s nam nlv num)"
  {
    have p1: "butlast (pools ?t) = pools s" unfolding K_MEM_POOL_DEFINE_def Let_def by auto
    with p0 have p2: "\<forall>p. p \<in> set (butlast (pools ?t)) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). block_state b)" by auto
    moreover
    have p3: "\<forall>b \<in> set (zerolevelblocklist (last (pools ?t))). b = (Leaf a) \<and> fst (snd a) = FREE" sorry   
    have p4: "b = Leaf a \<and> fst (snd a) = FREE \<longrightarrow> block_state b" unfolding block_state_def by auto
    with p3 have p5: "\<forall>b \<in> set (zerolevelblocklist (last (pools ?t))). block_state b" by auto
    moreover
    have p6: "pools ?t = append (butlast (pools ?t)) [(last (pools ?t))]" unfolding K_MEM_POOL_DEFINE_def Let_def by auto
    with p2 p5 have "\<forall>p. p \<in> set (pools ?t) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). block_state b)"
      by (smt butlast.simps(2) butlast_append in_set_butlastD in_set_conv_decomp_last last.simps last_appendR list.distinct(1))  
  }
  then show ?thesis unfolding inv_block_state_def by auto
qed
  
lemma inv_block_k_mem_pool_alloc: "s \<in> inv1_set \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv1_set" sorry
    
lemma inv_block_k_mem_pool_free: "s \<in> inv1_set \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv1_set" sorry
  
lemma inv_block_time_tick: "s \<in> inv_block_state \<Longrightarrow> time_tick s \<in> inv_block_state"
  unfolding time_tick_def Let_def inv_block_state_def block_state_def by auto
         
lemma inv_block_schedule: "s \<in> inv_block_state \<Longrightarrow> schedule s \<in> inv_block_state"
  unfolding schedule_def Let_def inv_block_state_def block_state_def by auto

lemma inv_block_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv_block_state \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv_block_state))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv_block_state"
    then have "\<forall>i<length ts. ts ! i \<in> inv_block_state"
      apply(induct ts)
       apply simp
      using inv_block_k_mem_pool_define inv_block_k_mem_pool_alloc inv_block_k_mem_pool_free inv_block_time_tick inv_block_schedule
      apply (metis One_nat_def Suc_less_eq Suc_pred length_Cons neq0_conv nth.simps nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_block_k_mem_pool_alloc length_Cons neq0_conv nth.simps nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_block_k_mem_pool_free length_Cons neq0_conv nth.simps nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_block_time_tick length_Cons neq0_conv nth_Cons')
      by (metis One_nat_def Suc_less_eq Suc_pred inv_block_schedule length_Cons neq0_conv nth_Cons')  
  }
  then show ?thesis by auto
qed
  
lemma inv_block_lm: "ReachStates \<subseteq> inv_block_state"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv_block_state" using inv_block_lm_helper inv_block_s0
    by (metis append_butlast_last_id exec_not_empty length_append_singleton lessI nth_append_length)
  }
  then show ?thesis by auto
qed
  
subsection \<open>def and proof of inv_block_level\<close>

primrec inv_level :: "Block \<Rightarrow> bool"
  where "inv_level (Leaf a) = True" |
        "inv_level (Node a ll lr rl rr) = (let lh = Suc (get_level (Node a ll lr rl rr)) in
                                     (lh = (get_level ll)) \<and> (lh = (get_level lr)) \<and> (lh = (get_level rl)) \<and> (lh = (get_level rr)) \<and> (inv_level ll \<and> inv_level lr \<and> inv_level rl \<and> inv_level rr))"

definition "inv_block_level \<equiv> {s::State. (\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). inv_level b))}"

lemma inv_level_s0: "s0 \<in> inv_block_level"
  unfolding s0_def inv_block_level_def inv_level_def using s0_def poolsinit by auto
    
lemma inv_level_k_mem_pool_define: "s \<in> inv_block_level \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv_block_level"
proof -
  assume "s \<in> inv_block_level"
  hence p0: "\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). inv_level b)" 
    unfolding inv_block_level_def by auto
  let ?t = "fst (K_MEM_POOL_DEFINE s nam nlv num)"
  {
    have p1: "butlast (pools ?t) = pools s" unfolding K_MEM_POOL_DEFINE_def Let_def by auto
    with p0 have p2: "\<forall>p. p \<in> set (butlast (pools ?t)) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). inv_level b)" by auto
    moreover
    have p3: "\<forall>b \<in> set (zerolevelblocklist (last (pools ?t))). b = (Leaf a)" sorry
    have p4: "b = Leaf a \<longrightarrow> inv_level b" unfolding inv_level_def by auto
    with p3 have p5: "\<forall>b \<in> set (zerolevelblocklist (last (pools ?t))). inv_level b" by auto
    moreover
    have p6: "pools ?t = append (butlast (pools ?t)) [(last (pools ?t))]" unfolding K_MEM_POOL_DEFINE_def Let_def by auto
    with p2 p5 have "\<forall>p. p \<in> set (pools ?t) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). inv_level b)"
      by (smt butlast.simps(2) butlast_append in_set_butlastD in_set_conv_decomp_last last.simps last_appendR list.distinct(1))  
  }
  then show ?thesis unfolding inv_block_level_def by auto
qed
    
lemma inv_level_k_mem_pool_alloc: "s \<in> inv_block_level \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv_block_level" sorry
    
lemma inv_level_k_mem_pool_free: "s \<in> inv_block_level \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv_block_level" sorry
  
lemma inv_level_time_tick: "s \<in> inv_block_level \<Longrightarrow> time_tick s \<in> inv_block_level"
  unfolding time_tick_def Let_def inv_block_level_def inv_level_def by auto
         
lemma inv_level_schedule: "s \<in> inv_block_level \<Longrightarrow> schedule s \<in> inv_block_level"
  unfolding schedule_def Let_def inv_block_level_def inv_level_def by auto
        
lemma inv_level_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv_block_level \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv_block_level))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv_block_level"
    then have "\<forall>i<length ts. ts ! i \<in> inv_block_level"
      apply(induct ts)
       apply simp
      using inv_level_k_mem_pool_define inv_level_k_mem_pool_alloc inv_level_k_mem_pool_free inv_level_time_tick inv_level_schedule
      apply (metis One_nat_def Suc_less_eq Suc_pred length_Cons neq0_conv nth.simps nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_level_k_mem_pool_alloc length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_level_k_mem_pool_free length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_level_time_tick length_Cons neq0_conv nth_Cons')
      by (metis One_nat_def Suc_less_eq Suc_pred inv_level_schedule length_Cons neq0_conv nth_Cons')   
  }
  then show ?thesis by auto
qed
  
lemma inv_level_lm: "ReachStates \<subseteq> inv_block_level"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv_block_level" using inv_level_lm_helper inv_level_s0
    by (metis append_butlast_last_id exec_not_empty length_append_singleton lessI nth_append_length)
  }
  then show ?thesis by auto
qed

subsection \<open>def and proof of inv_block_free\<close>
        
primrec inv_free :: "Block \<Rightarrow> bool"
  where "inv_free (Leaf a) = True" |
        "inv_free (Node a ll lr rl rr) = (~((get_blocktype ll)=FREE \<and> (get_blocktype lr)=FREE \<and> (get_blocktype rl)=FREE \<and> (get_blocktype rr)=FREE) \<and> (inv_free ll) \<and> (inv_free lr) \<and> (inv_free rl) \<and> (inv_free rr))"

definition "inv_block_free \<equiv> {s::State. (\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). inv_free b))}"

lemma inv_free_s0: "s0 \<in> inv_block_free"
  unfolding s0_def inv_block_free_def inv_free_def using s0_def poolsinit by auto
    
lemma inv_free_k_mem_pool_define: "s \<in> inv_block_free \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv_block_free"
proof -
  assume "s \<in> inv_block_free"
  hence p0: "\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). inv_free b)" 
    unfolding inv_block_free_def by auto
  let ?t = "fst (K_MEM_POOL_DEFINE s nam nlv num)"
  {
    have p1: "butlast (pools ?t) = pools s" unfolding K_MEM_POOL_DEFINE_def Let_def by auto
    with p0 have p2: "\<forall>p. p \<in> set (butlast (pools ?t)) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). inv_free b)" by auto
    moreover
    have p3: "\<forall>b \<in> set (zerolevelblocklist (last (pools ?t))). b = (Leaf a)" sorry
    have p4: "b = Leaf a \<longrightarrow> inv_free b" unfolding inv_free_def by auto
    with p3 have p5: "\<forall>b \<in> set (zerolevelblocklist (last (pools ?t))). inv_free b" by auto
    moreover
    have p6: "pools ?t = append (butlast (pools ?t)) [(last (pools ?t))]" unfolding K_MEM_POOL_DEFINE_def Let_def by auto
    with p2 p5 have "\<forall>p. p \<in> set (pools ?t) \<longrightarrow> (\<forall>b \<in> set (zerolevelblocklist p). inv_free b)"
      by (smt butlast.simps(2) butlast_append in_set_butlastD in_set_conv_decomp_last last.simps last_appendR list.distinct(1))  
  }
  then show ?thesis unfolding inv_block_free_def by auto
qed  
    
lemma inv_free_k_mem_pool_alloc: "s \<in> inv_block_free \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv_block_free" sorry
    
lemma inv_free_k_mem_pool_free: "s \<in> inv_block_free \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv_block_free" sorry
  
lemma inv_free_time_tick: "s \<in> inv_block_free \<Longrightarrow> time_tick s \<in> inv_block_free"
  unfolding time_tick_def Let_def inv_block_free_def inv_free_def by auto
         
lemma inv_free_schedule: "s \<in> inv_block_free \<Longrightarrow> schedule s \<in> inv_block_free"
  unfolding schedule_def Let_def inv_block_free_def inv_free_def by auto
    
lemma inv_free_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv_block_free \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv_block_free))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv_block_free"
    then have "\<forall>i<length ts. ts ! i \<in> inv_block_free"
      apply(induct ts)
       apply simp
      using inv_free_k_mem_pool_define inv_free_k_mem_pool_alloc inv_free_k_mem_pool_free inv_free_time_tick inv_free_schedule
      apply (metis One_nat_def Suc_less_eq Suc_pred length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_free_k_mem_pool_alloc length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_free_k_mem_pool_free length_Cons neq0_conv nth.simps nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_free_time_tick length_Cons neq0_conv nth_Cons')
      by (metis One_nat_def Suc_less_eq Suc_pred inv_free_schedule length_Cons neq0_conv nth_Cons')
  }
  then show ?thesis by auto
qed

lemma inv_free_lm: "ReachStates \<subseteq> inv_block_free"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv_block_free" using inv_free_lm_helper inv_free_s0
    by (metis append_butlast_last_id exec_not_empty length_append_singleton lessI nth_append_length)
  }
  then show ?thesis by auto
qed

subsection \<open>def and proof of inv_n_levels\<close>

definition "inv_n_levels \<equiv> {s::State. (\<forall>p. p \<in> set (pools s) \<longrightarrow> length (freelist p) = n_levels p)}"  

lemma inv_n_levels_s0: "s0 \<in> inv_n_levels"
  unfolding s0_def inv_n_levels_def using s0_def poolsinit by auto
    
lemma inv_n_levels_k_mem_pool_define: "s \<in> inv_n_levels \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv_n_levels"
proof -
  assume "s \<in> inv_n_levels"
  hence p0: "\<forall>p. p \<in> set (pools s) \<longrightarrow> length (freelist p) = n_levels p" 
    unfolding inv_n_levels_def by auto
  let ?t = "fst (K_MEM_POOL_DEFINE s nam nlv num)"
  {
    have p1: "butlast (pools ?t) = pools s" unfolding K_MEM_POOL_DEFINE_def Let_def by auto
    with p0 have p2: "\<forall>p. p \<in> set (butlast (pools ?t)) \<longrightarrow> length (freelist p) = n_levels p" by auto
    moreover
    have p3: "p = last (pools ?t) \<longrightarrow> length (freelist p) = n_levels p" sorry
    moreover
    have p4: "pools ?t = append (butlast (pools ?t)) [(last (pools ?t))]" unfolding K_MEM_POOL_DEFINE_def Let_def by auto
    with p2 p3 have "\<forall>p. p \<in> set (pools ?t) \<longrightarrow> length (freelist p) = n_levels p" sorry
  }
  then show ?thesis unfolding inv_n_levels_def by auto
qed   
    
lemma inv_n_levels_k_mem_pool_alloc: "s \<in> inv_n_levels \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv_n_levels" sorry
    
lemma inv_n_levels_k_mem_pool_free: "s \<in> inv_n_levels \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv_n_levels" sorry
  
lemma inv_n_levels_time_tick: "s \<in> inv_n_levels \<Longrightarrow> time_tick s \<in> inv_n_levels"
  unfolding time_tick_def Let_def inv_n_levels_def by auto
         
lemma inv_n_levels_schedule: "s \<in> inv_n_levels \<Longrightarrow> schedule s \<in> inv_n_levels"
  unfolding schedule_def Let_def inv_n_levels_def by auto
   
lemma inv_n_levels_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv_n_levels \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv_n_levels))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv_n_levels"
    then have "\<forall>i<length ts. ts ! i \<in> inv_n_levels"
      apply(induct ts)
       apply simp
      using inv_n_levels_k_mem_pool_define inv_n_levels_k_mem_pool_alloc inv_n_levels_k_mem_pool_free inv_n_levels_time_tick inv_n_levels_schedule
      apply (metis (no_types, lifting) diff_less length_Cons less_Suc_eq less_le_trans less_one nat_less_le neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_n_levels_k_mem_pool_alloc length_Cons neq0_conv nth.simps nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_n_levels_k_mem_pool_free length_Cons neq0_conv nth.simps nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_n_levels_time_tick length_Cons neq0_conv nth_Cons')
      by (metis One_nat_def Suc_less_eq Suc_pred inv_n_levels_schedule length_Cons neq0_conv nth_Cons')    
  }
  then show ?thesis by auto
qed
    
lemma inv_n_levels_lm: "ReachStates \<subseteq> inv_n_levels"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv_n_levels" using inv_n_levels_lm_helper inv_n_levels_s0
    by (metis append_butlast_last_id exec_not_empty length_append_singleton lessI nth_append_length)
  }
  then show ?thesis by auto
qed

subsection \<open>def and proof of inv_nmax\<close>

definition "inv_nmax \<equiv> {s::State. (\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>i<length (freelist p). length ((freelist p) ! i) \<le> (nmax p)*4^i))}"
  
lemma inv_nmax_s0: "s0 \<in> inv_nmax"
  unfolding s0_def inv_nmax_def using s0_def poolsinit by auto
    
lemma inv_nmax_k_mem_pool_define: "s \<in> inv_nmax \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv_nmax" sorry
    
lemma inv_nmax_k_mem_pool_alloc: "s \<in> inv_nmax \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv_nmax" sorry
    
lemma inv_nmax_k_mem_pool_free: "s \<in> inv_nmax \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv_nmax" sorry
  
lemma inv_nmax_time_tick: "s \<in> inv_nmax \<Longrightarrow> time_tick s \<in> inv_nmax"
  unfolding time_tick_def Let_def inv_nmax_def by auto
         
lemma inv_nmax_schedule: "s \<in> inv_nmax \<Longrightarrow> schedule s \<in> inv_nmax"
  unfolding schedule_def Let_def inv_nmax_def by auto
  
lemma inv_nmax_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv_nmax \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv_nmax))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv_nmax"
    then have "\<forall>i<length ts. ts ! i \<in> inv_nmax"
      apply(induct ts)
       apply simp
      using inv_nmax_k_mem_pool_define inv_nmax_k_mem_pool_alloc inv_nmax_k_mem_pool_free inv_nmax_time_tick inv_nmax_schedule
      apply (metis One_nat_def Suc_less_eq Suc_pred length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_nmax_k_mem_pool_alloc length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_nmax_k_mem_pool_free length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv_nmax_time_tick length_Cons neq0_conv nth_Cons')
      by (metis One_nat_def Suc_less_eq Suc_pred inv_nmax_schedule length_Cons neq0_conv nth_Cons')
  }
  then show ?thesis by auto
qed
  
lemma inv_nmax_lm: "ReachStates \<subseteq> inv_nmax"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv_nmax" using inv_nmax_lm_helper inv_nmax_s0
    by (metis append_butlast_last_id exec_not_empty length_append_singleton lessI nth_append_length)
  }
  then show ?thesis by auto
qed

subsection \<open>def and proof of inv7\<close>
  
primrec inv7 :: "Block \<Rightarrow> ID \<Rightarrow> nat \<Rightarrow> bool"
  where "inv7 (Leaf a) num lv = ((snd (snd a) = num) \<and> (get_blocktype (Leaf a) = FREE) \<and> (get_level (Leaf a) = lv))" |
        "inv7 (Node a ll lr rl rr) num lv = ( inv7 ll num lv \<or> inv7 lr num lv \<or> inv7 rl num lv \<or> inv7 rr num lv)"
        
definition "inv7_set \<equiv> {s::State. (\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>l<n_levels p. \<forall>i\<in>(set ((freelist p)!l)). \<exists>b\<in>set ((zerolevelblocklist p)). inv7 b i l))}"
  
lemma inv7_s0: "s0 \<in> inv7_set"
  unfolding s0_def inv7_set_def inv7_def using s0_def poolsinit by auto
    
lemma inv7_k_mem_pool_define: "s \<in> inv7_set \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv7_set" sorry
    
lemma inv7_k_mem_pool_alloc: "s \<in> inv7_set \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv7_set" sorry
    
lemma inv7_k_mem_pool_free: "s \<in> inv7_set \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv7_set" sorry
  
lemma inv7_time_tick: "s \<in> inv7_set \<Longrightarrow> time_tick s \<in> inv7_set"
  unfolding time_tick_def Let_def inv7_set_def inv7_def by auto
         
lemma inv7_schedule: "s \<in> inv7_set \<Longrightarrow> schedule s \<in> inv7_set"
  unfolding schedule_def Let_def inv7_set_def inv7_def by auto
    
lemma inv7_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv7_set \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv7_set))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv7_set"
    then have "\<forall>i<length ts. ts ! i \<in> inv7_set"
      apply(induct ts)
       apply simp
      using inv7_k_mem_pool_define inv7_k_mem_pool_alloc inv7_k_mem_pool_free inv7_time_tick inv7_schedule
      apply (metis One_nat_def Suc_less_eq Suc_pred length_Cons neq0_conv nth_Cons')
      apply (metis inv7_k_mem_pool_alloc length_Cons less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc)
      apply (metis inv7_k_mem_pool_free length_Cons less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc)
      apply (metis One_nat_def Suc_less_eq Suc_pred inv7_time_tick length_Cons neq0_conv nth_Cons')
      by (metis One_nat_def Suc_less_eq Suc_pred inv7_schedule length_Cons neq0_conv nth_Cons')   
  }
  then show ?thesis by auto
qed    
    
lemma inv7_lm: "ReachStates \<subseteq> inv7_set"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv7_set" using inv7_lm_helper inv7_s0
    by (metis append_butlast_last_id exec_not_empty length_append_singleton lessI nth_append_length)
  }
  then show ?thesis by auto
qed

subsection \<open>def and proof of inv8\<close>
  
primrec inv8 :: "Block \<Rightarrow> nat \<Rightarrow> ID list"
  where "inv8 (Leaf a) lv = (if get_level (Leaf a) = lv \<and> get_blocktype (Leaf a) = FREE then [snd (snd a)] else [])" |
        "inv8 (Node a ll lr rl rr) lv = (inv8 ll lv @ inv8 lr lv @ inv8 rl lv @ inv8 rr lv)"
             
definition "inv8_set \<equiv> {s::State. (\<forall>p. p \<in> set (pools s) \<longrightarrow> (\<forall>b\<in>set(zerolevelblocklist p). \<forall>l<n_levels p. set (inv8 b l) \<subset> set ((freelist p) ! l)))}"

lemma inv8_s0: "s0 \<in> inv8_set"
  unfolding s0_def inv8_set_def inv8_def using s0_def poolsinit by auto
    
lemma inv8_k_mem_pool_define: "s \<in> inv8_set \<Longrightarrow> fst (K_MEM_POOL_DEFINE s nam nlv num) \<in> inv8_set" sorry
    
lemma inv8_k_mem_pool_alloc: "s \<in> inv8_set \<Longrightarrow> fst (k_mem_pool_alloc s po lv ti) \<in> inv8_set" sorry
    
lemma inv8_k_mem_pool_free: "s \<in> inv8_set \<Longrightarrow> fst (k_mem_pool_free s po num) \<in> inv8_set" sorry
  
lemma inv8_time_tick: "s \<in> inv8_set \<Longrightarrow> time_tick s \<in> inv8_set"
  unfolding time_tick_def Let_def inv8_set_def inv8_def by auto
         
lemma inv8_schedule: "s \<in> inv8_set \<Longrightarrow> schedule s \<in> inv8_set"
  unfolding schedule_def Let_def inv8_set_def inv8_def by auto
    
lemma inv8_lm_helper: "\<forall>ts. (ts \<in> execution \<and> ts ! 0 \<in> inv8_set \<longrightarrow> (\<forall>i<length ts. ts ! i \<in> inv8_set))"
proof -
  {
    fix ts
    assume p0: "ts \<in> execution"
       and p1: "ts ! 0 \<in> inv8_set"
    then have "\<forall>i<length ts. ts ! i \<in> inv8_set"
      apply(induct ts)
       apply simp
      using inv8_k_mem_pool_define inv8_k_mem_pool_alloc inv8_k_mem_pool_free inv8_time_tick inv8_schedule
      apply (metis One_nat_def Suc_less_eq Suc_pred length_Cons neq0_conv nth_Cons')
      apply (metis inv8_k_mem_pool_alloc length_Cons less_Suc_eq_0_disj nth_Cons_0 nth_Cons_Suc)
      apply (metis One_nat_def Suc_less_eq Suc_pred inv8_k_mem_pool_free length_Cons neq0_conv nth_Cons')
      apply (metis One_nat_def Suc_less_eq Suc_pred inv8_time_tick length_Cons neq0_conv nth_Cons')
      by (metis One_nat_def Suc_less_eq Suc_pred inv8_schedule length_Cons neq0_conv nth_Cons')   
  }
  then show ?thesis by auto
qed    
  
lemma inv8_lm: "ReachStates \<subseteq> inv8_set"
proof -
  {
    fix s
    assume p0: "s \<in> ReachStates"
    hence "reachable0 s" by (simp add:ReachStates_def)
    hence "reachable s0 s" by (simp add:reachable0_def)
    hence "\<exists>ts \<in> execution. ts ! 0 = s0 \<and> last ts = s" by (simp add:reachable_def)
    then obtain ts where a1: "ts \<in> execution" and a2: "ts ! 0 = s0" and a3: "last ts = s" by auto
    hence "s \<in> inv8_set" using inv8_lm_helper inv8_s0
    by (metis append_butlast_last_id exec_not_empty length_append_singleton lessI nth_append_length)     
  }
  then show ?thesis by auto
qed  
  
end